/*
** configset.hh
** Login : <David@sandrock.lrde.epita.fr>
** Started on  Mon Apr  7 13:42:20 2003 David Lesage
** $Id: configset.hh 53 2003-06-10 17:17:54Z burrus_n $
** 
** Copyright (C) 2003 David Lesage
** This program is free software; you can redistribute it and/or modify
** it under the terms of the GNU General Public License as published by
** the Free Software Foundation; either version 2 of the License, or
** (at your option) any later version.
** 
** This program is distributed in the hope that it will be useful,
** but WITHOUT ANY WARRANTY; without even the implied warranty of
** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
** GNU General Public License for more details.
** 
** You should have received a copy of the GNU General Public License
** along with this program; if not, write to the Free Software
** Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
*/

#ifndef   	CONFIGSET_HH_
# define   	CONFIGSET_HH_

# include <iostream>

# include <boost/dynamic_bitset.hpp>

# include "common.hh"
# include "config.hh"
# include "initializer.hh"
# include "varset.hh"

namespace evz
{

  /*-------------.
  | ConfigSet<T> |
  `-------------*/

  //! Represet a set of Configs.
  /*!  
    bitsets are used to reprensent the configs which are included
    in the set. One bit corresponds to one configuration. The size of
    the bitset is the total number of possible configurations on the
    given VarSet.
  */

  template <class T>
  class ConfigSet
  {
  private:
    typedef Initializer<Config<T> > initializer_type;

  public:
    struct const_iterator
    {
      const_iterator(const ConfigSet<T>& obj, unsigned index = 0)
	: obj_(obj), cur_index_(index) 
      {
	cur_index_ = obj_.get_next_activated_bit(index);
      }

      bool operator==(const const_iterator& rhs) const
      {
	return (rhs.cur_index_ == cur_index_)
	  && (&(rhs.obj_) == &obj_);
      }

      bool operator!=(const const_iterator& rhs) const
      {
	return !(*this == rhs);
      }

      const const_iterator& operator++()
      {
	cur_index_ = obj_.get_next_activated_bit(cur_index_ + 1);
	return *this;
      }

      const_iterator operator++(int)
      {
	const_iterator tmp(*this);
	cur_index_ = obj_.get_next_activated_bit(cur_index_ + 1);
	return tmp;
      }
      
      Config<T> operator*() const
      {
	return obj_.get_config(cur_index_);
      }

    private:
      const ConfigSet<T>& obj_;
      unsigned cur_index_;
    };

  public:
    ConfigSet(const VarSet<T>& vs)
      : vset_(vs), configs_(vs.get_nb_configs())
    {}

    // Return a starter for the list of realisations.
    static initializer_type start()
    {
      return initializer_type();
    }

    // Iterators accessors
    const_iterator begin() const
    {
      return const_iterator(*this, 0);
    }
    const_iterator end() const
    {
      return const_iterator(*this, size());
    }

    // Add a list of configs into the set.
    void add_configs(const initializer_type& configs)
    {
      for (typename initializer_type::const_iterator config = configs.begin();
	   config != configs.end();
	   ++config)
	add_config(*config);
    }

    // Add a new Config into the set.
    void add_config(const Config<T>& config)
    {
      configs_.set(get_index(config));
    }

    // Remove a config from the set.
    void remove_config(const Config<T>& config)
    {
      configs_.reset(get_index(config));
    }

    // Add all possible configs to the set. This is useful to
    // construct the complete frame of discernement.
    void add_all_configs()
    {
      configs_.set();
    }

    // Return the intersection with another ConfigSet.
    ConfigSet<T> operator&(const ConfigSet& s) const
    {
      assert (vset_ == s.vset_);
      return ConfigSet<T>(vset_, configs_ & s.configs_);
    }

    // Intersect with another ConfigSet.
    ConfigSet<T>& operator&=(const ConfigSet& s)
    {
      assert(vset_ == s.vset_);
      configs_ &= s.configs_;
      return *this;
    }
    
    // Return the union with another ConfigSet.
    ConfigSet<T> operator|(const ConfigSet& s) const
    {
      assert(vset_ == s.vset_);  
      return configs_ | s.configs_;
    }

    // Make the union with another ConfigSet.
    ConfigSet<T>& operator|=(const ConfigSet& s)
    {
      assert(vset_ == s.vset_);    
      configs_ |= s.configs_;
      return *this;
    }

    // An arbitrary order on ConfigSet is needed to create hash
    // tables.
    bool operator<(const ConfigSet<T>& cs) const
    {
      return configs_ < cs.configs_;
    }
    
    bool operator==(const ConfigSet<T>& cs) const
    {
      return configs_ == cs.configs_;
    } 

    bool operator!=(const ConfigSet<T>& cs) const
    {
      return configs_ != cs.configs_;
    } 

    bool is_subset_of(const ConfigSet<T>& cs) const
    {
      return configs_.is_subset_of(cs.configs_);
    }

    bool has(const Config<T>& config) const
    {
      return configs_.test(get_index(config));
    }

    // Return true is there is a non empty intersection with the given
    // ConfigSet.
    bool intersect_with(const ConfigSet<T>& cs) const
    {
      return !(configs_ & cs.configs_).none();
    }

    // Return the cardinal of the configset
    unsigned card() const
    {
      return get_nb_configs();
    }
        
    // Return the number of Config in the set.
    unsigned get_nb_configs() const
    {
      return configs_.count();
    }

    // Return the total number of possible configs.
    unsigned size() const
    {
      return configs_.size();
    }

    const VarSet<T>& get_varset(void) const
    {
      return vset_;
    }

    // n is not a config index in the bitset, but the nth set config.
    Config<T> get_nth_config(unsigned n) const
    {
      assert(n < size());
    
      unsigned cpt = 0; // current config num
      unsigned cpt2 = 0; // current config index
    
      for (; cpt2 < configs_.size(); ++cpt2)
	{
	  if (configs_[cpt2])
	    {
	      if (cpt == n)
		break;
	      ++cpt;
	    }
	};
    
      assert(cpt2 < configs_.size());
    
      return get_config(cpt2);
    }

    // Return a new configset projected on the varset without x.
    ConfigSet<T> get_sproj(const Var<T>& x) const
    {
      assert(vset_.has_var(x));
      
      VarSet<T> vs(vset_);
      vs.del_var(x);
      
      ConfigSet<T> res(vs);
      ConfigSet<T> tmp(*this);

      unsigned rank = x.get_rank();
      unsigned u = rank > 0 ? vset_.get_nb_configs(0, rank - 1) : 1; //FIXME: why 1 ?
      unsigned v = vset_.get_nb_configs(rank + 1, vset_.get_max_rank());
      
      for (unsigned k = 0; k < x.size() - 1; ++k)
	tmp.configs_ |= (tmp.configs_ >> v);

      for (unsigned k = 0; k < u; ++k)
	res.deposit(v, k * v, tmp.extract(v, k * v * x.size())); 

      return res;
    }

    // Return a new configset quasi-projected on the varset without x.
    // FIXME: validate
    ConfigSet<T> get_sqproj(const Var<T>& x) const
    {
      assert(vset_.has_var(x));
      
      ConfigSet<T> res(*this);

      unsigned rank = x.get_rank();
      unsigned u = rank > 0 ? vset_.get_nb_configs(0, rank - 1) : 1; //FIXME: why 1 ?
      unsigned v = vset_.get_nb_configs(rank + 1, vset_.get_max_rank());
      
      for (unsigned k = 0; k < x.size() - 1; ++k)
	res.configs_ |= (res.configs_ >> v);
 
      bitset mask(configs_.size());
      for (unsigned k = 0; k < u; ++k)
	{
	  unsigned pos = k * v * x.size();	  
	  for (unsigned i = pos; i < pos + v; i++)
	    mask[i] = 1;
	}
      res.configs_ &= mask;
      
      for (unsigned k = 0; k < x.size() - 1; ++k)
	res.configs_ |= (res.configs_ << v);

      return res;
    }


    // Apply a simple projection, removing var x.
    // FIXME: optimize
    ConfigSet<T>& sproj(const Var<T>& x)
    {
      assert(vset_.has_var(x));
      
      VarSet<T> vs(vset_);
      vs.del_var(x);
      
      ConfigSet<T> res(vs);
      ConfigSet<T> tmp(*this);

      unsigned rank = x.get_rank();
      unsigned u = rank > 0 ? vset_.get_nb_configs(0, rank - 1) : 1;
      unsigned v = vset_.get_nb_configs(rank + 1, vset_.get_max_rank());
      
      for (unsigned k = 0; k < x.size() - 1; ++k)
	tmp.configs_ |= (tmp.configs_ >> v);

      for (unsigned k = 0; k < u; ++k)
	res.deposit(v, k * v, tmp.extract_and_reset(v, k * v * x.size())); 

      configs_ = res.configs_;
      vset_.del_var(x);

      return *this;
    }


    // Apply a simple quasi-projection without var x.
    // FIXME: validate & optimize
    ConfigSet<T>& sqproj(const Var<T>& x)
    {
      assert(vset_.has_var(x));
      
      unsigned rank = x.get_rank();
      unsigned u = rank > 0 ? vset_.get_nb_configs(0, rank - 1) : 1; 
      unsigned v = vset_.get_nb_configs(rank + 1, vset_.get_max_rank());
      
      for (unsigned k = 0; k < x.size() - 1; ++k)
	configs_ |= (configs_ >> v);
 
      bitset mask(configs_.size());
      for (unsigned k = 0; k < u; ++k)
	{
	  unsigned pos = k * v * x.size();	  
	  for (unsigned i = pos; i < pos + v; i++)
	    mask[i] = 1;
	}
      configs_ &= mask;
      
      for (unsigned k = 0; k < x.size() - 1; ++k)
	configs_ |= (configs_ << v);

      return *this;
    }


    // Return a new configset, result the simple extension of this with x.
    ConfigSet<T> get_sext(const Var<T>& x) const
    {
      assert(!vset_.has_var(x));
      
      VarSet<T> vs(vset_);
      vs.add_var(x);
      
      ConfigSet<T> res(vs);

      unsigned rank = x.get_rank();
      unsigned u = rank > 0 ? vset_.get_nb_configs(0, rank - 1) : 1;
      unsigned v = vset_.get_nb_configs(rank + 1, vset_.get_max_rank());

      for (unsigned k = 0; k < u; ++k)
	res.deposit(v, k * x.size() * v, extract(v, k * v));

      for (unsigned k = 0; k < x.size() - 1; ++k)
	res.configs_ |= (res.configs_ << v);

      return res;
    }

    // Apply an extension, adding var x.
    // FIXME: optimize
    ConfigSet<T>& sext(const Var<T>& x) 
    {      
      assert(!vset_.has_var(x));
      
      VarSet<T> vs(vset_);
      vs.add_var(x);
      
      ConfigSet<T> res(vs);

      unsigned rank = x.get_rank();
      unsigned u = rank > 0 ? vset_.get_nb_configs(0, rank - 1) : 1;
      unsigned v = vset_.get_nb_configs(rank + 1, vset_.get_max_rank());

      for (unsigned k = 0; k < u; ++k)
	res.deposit(v, k * x.size() * v, extract_and_reset(v, k * v));

      for (unsigned k = 0; k < x.size() - 1; ++k)
	res.configs_ |= (res.configs_ << v);

      vset_.add_var(x);
      configs_ = res.configs_;

      return *this;
    }
    
    // Return a new ConfigSet, projected on the given VarSet.
    ConfigSet<T> get_proj(const VarSet<T>& s) const
    {
      assert(s.is_subset_of(vset_));
 
      if (s == vset_)
	return *this;

      ConfigSet<T> tmp(*this);
 
      for (unsigned u = 0; u < vset_.size(); u++)
	if (vset_.has_var(u) && !s.has_var(u))
	  tmp.sproj(vset_.get_var(u));
      return tmp;
    }

    // Return a new ConfigSet, quasi-projected on the given VarSet.
    ConfigSet<T> get_qproj(const VarSet<T>& s) const
    {
      assert(s.is_subset_of(vset_));
 
      if (s == vset_)
	return *this;

      ConfigSet<T> tmp(*this);
 
      for (unsigned u = 0; u < vset_.size(); u++)
	if (vset_.has_var(u) && !s.has_var(u))
	  tmp.sqproj(vset_.get_var(u));
      return tmp;
    }

    // Return a new ConfigSet, extended on the given VarSet.
    ConfigSet<T> get_ext(const VarSet<T>& s) const
    {
      assert(vset_.is_subset_of(s));
      
      if (s == vset_)
	return *this;

      ConfigSet<T> tmp(*this);
   
      for (unsigned u = 0; u < vset_.size(); ++u)
	if (!vset_.has_var(u) && s.has_var(u))
	  tmp.sext(vset_.get_var(u));
      return tmp;
    }

    // Apply a projection on the given VarSet.
    ConfigSet<T>& proj(const VarSet<T>& s) 
    {
      assert(s.is_subset_of(vset_));
 
      if (s == vset_)
	return *this;

      unsigned vset_size = vset_.size();
      for (unsigned u = 0; u < vset_size; u++)
	if (vset_.has_var(u) && !s.has_var(u))
	  sproj(vset_.get_var(u));
      return *this;
    }

    // Apply a quasi-projection on the given VarSet.
    ConfigSet<T>& qproj(const VarSet<T>& s) 
    {
      assert(s.is_subset_of(vset_));
 
      if (s == vset_)
	return *this;

      unsigned vset_size = vset_.size();
      for (unsigned u = 0; u < vset_size; u++)
	if (vset_.has_var(u) && !s.has_var(u))
	  sqproj(vset_.get_var(u));
      return *this;
    }


    // Apply an extension on the given VarSet.
    ConfigSet<T>& ext(const VarSet<T>& s) 
    {
      assert(vset_.is_subset_of(s));

      if (s == vset_)
	return *this;

      unsigned vset_size = vset_.size();
      for (unsigned u = 0; u < vset_size; ++u)
	if (!vset_.has_var(u) && s.has_var(u))
	  sext(vset_.get_var(u));
      return *this;
    }

    // Print the configset in a stream.
    void print(std::ostream& o) const
    {
      unsigned cpt = 0;
      o << "{ ";
      for (unsigned i = 0; i < size(); ++i)
	if (configs_[i])
	  {
	    o << get_config(i);
	    if (cpt < get_nb_configs() - 1)
	      o << ", ";
	    ++cpt;
	  }
      o << " }";
    }

  private:
    ConfigSet(const VarSet<T>& vs, const bitset& configs)
      : vset_(vs), configs_(configs)
    {}

    // Return the internal index in the bitset associated to the config.
    unsigned get_index(const Config<T>& c) const
    {
      unsigned res = 0;
      unsigned curvar = 0;
      for (typename Config<T>::const_iterator it = c.get_values().begin();
	   it != c.get_values().end(); ++it, ++curvar)
	{
	  // FIXME: OPTIMIZE
	  unsigned pi = 1;
	  for (unsigned i = curvar + 1; i < c.get_values().size(); i++)
	    pi *= vset_.get_nth_var(i).size();

	  res += (*it) * pi;
	}
      return res;
    }

    // Return the next bit activated in the configset
    unsigned get_next_activated_bit(unsigned index) const
    {
      for (unsigned i = index; i < size(); ++i)
	if (configs_.test(i))
	  return i;
      return size();
    }

    // Return a Config instance associated to a bitset index.
    Config<T> get_config(unsigned index) const
    {
      return Config<T>(vset_, get_values(index));
    }

    // Return a list of values from the given bitset index.  FIXME:
    // why does ConfigSet has to know about T ? Shouldn't it return a
    // list of value id ?
    std::list<T> get_values(unsigned index) const
    {
      typename std::list<T> res;
      unsigned cpt = vset_.size();
    
      for (; cpt > 0; --cpt)
	{
	  if (vset_.has_var(cpt-1))
	    {
	      unsigned new_val = index % vset_.get_var(cpt-1).size();
	      index /= vset_.get_var(cpt-1).size();
	      res.push_front(vset_.get_var(cpt-1).get_real(new_val));
	    }
	}

      return res;
    }    

    // Return a new bitset, filled with nb bits of configs starting at pos.
    bitset extract(unsigned nb, unsigned pos) const
    {

      bitset mask(configs_.size());
      for (unsigned i = pos; i < pos + nb; i++)
	mask[i] = 1;

      bitset res = configs_ & mask;
      res >>= pos;

      return res;
    }

    // Return a new bitset, filled with nb bits of configs starting at pos.
    // After that, the nb bits extracted are cleared in configs_.
    bitset extract_and_reset(unsigned nb, unsigned pos) 
    {
      bitset mask(configs_.size());
      for (unsigned i = pos; i < pos + nb; i++)
	mask[i] = 1;

      bitset res = configs_ & mask;
      mask.flip();
      configs_ &= mask;
      res >>= pos;
      return res;
    }


    // Put the first nb bits of rhs in configs_, starting at the given pos.
    void deposit(unsigned nb, unsigned pos, const bitset& rhs)
    {
      // FIXME: this implementation is perhaps not yet optimal !
      
      // nmask is all 0 except for n bits starting at pos which are at 1
      bitset nmask(configs_.size());
      nmask.flip();
      for (unsigned i = pos; i < pos + nb; i++)
	nmask[i] = 0;
      
      // new_bits is filled with 0 except for n bits starting at pos which
      // copy the n first bits of rhs.
      bitset new_bits = rhs;
      new_bits.resize(configs_.size());
      new_bits <<= pos;
      
      configs_ &= nmask;
     
      configs_ |= new_bits;
    }

  private:
    VarSet<T> vset_;
    bitset configs_;
  };

  template<class T>
  inline std::ostream&
  operator<<(std::ostream& o, const ConfigSet<T>& cs)
  {
    cs.print(o);
    return o;
  }

} // end of namespace evz

#endif	    /* !CONFIGSET_HH_ */
